-- Vill göra: hash-tabell/map istället för lista med axiom i bevis
-- Det ska gå att göra typ

{-

Give me theorem.
Prover> ([p] ==> [q], p, [q] <=> [r]) -> r
Ok. Prove theorem.
Prover> ImplE (p, [p] ==> [q]) q
Valid. Next?
Prover> :gifTrue
Axioms and conclusions: 
([p] ==> [q], p, [q] <=> [r], q)
Now finish your proof.
Prover> ImplE (q, [p] <=> [r]) r
Valid. Nice. Proof accepted. Next theorem?

-}
-- genom att hasha eller mappa WFF:sen på något sätt.
-- Alex 
-- ==================================================
-- a logic module
module Prover(
  module Data.Map
  ,module Data.List
  ,WFF(..)
  ,Theorem(..)
--  ,Proof(..)
--  ,check_proof
  ) where
import qualified Data.List
import Data.Map(Map, (!), fromList)

-- ==================================================
-- Well Formed Formula
data WFF = TRUE | FALSE
         | WFFvar String
         | And WFF WFF
         | Or WFF WFF
         | Not WFF
         | Imp WFF WFF
         | Equ WFF WFF
           deriving Eq
                    
evaluateMap :: Map String Bool -> WFF -> Bool
evaluateMap _ TRUE = True
evaluateMap _ FALSE = False
evaluateMap m (WFFvar st) = m!st
evaluateMap m (And p q) = (evaluateMap m p) && (evaluateMap m q)
evaluateMap m (Or p q) = (evaluateMap m p) || (evaluateMap m q)
evaluateMap m (Not p) = not (evaluateMap m p)
evaluateMap m (Imp p q) = if 
  ((evaluateMap m p) && not (evaluateMap m q)) 
                       then False
                       else True
evaluateMap m (Equ p q) = (evaluateMap m p) /= (evaluateMap m q)

evaluate :: [(String,Bool)] -> WFF -> Bool
evaluate st r = evaluateMap (fromList st) r

-- ==================================================            
instance Show WFF where
  show TRUE = "True"
  show FALSE = "False"
  show (WFFvar x) = x
  show (And p q) = "(" ++ (show p) ++ " && " ++ (show q) ++ ")"
  show (Or p q) = "(" ++ (show p) ++ " || " ++ (show q) ++ ")"
  show (Not p) = "!(" ++ (show p) ++ ")"
  show (Imp p q) = "[" ++ (show p) ++ "] ==> [" ++ (show q) ++ "]"
  show (Equ p q) = "[" ++ (show p) ++ "] <=> [" ++ (show q) ++ "]"
  
-- ==================================================  
-- instance Read WFF where
-- Read needs something else than just (read :: String -> WFF)
  
str2WFF = (str2WFFHelp . (filter (/=' ') ))

str2WFFHelp "True" = TRUE
str2WFFHelp "False" = FALSE

-- if the first is "(" and last ")" then find the operators inside 
-- and split string
str2WFFHelp xs = case xs of
  all@('(':xs) -> if (last xs /= ')') 
              then error "Parse error/n"
              else if (operator == '&') 
                   then And (str2WFFHelp before) (str2WFFHelp after)
                   else if (operator == '|')
                        then Or (str2WFFHelp before) (str2WFFHelp after)
                        else error "Parse error\n"
    where before = substring 2 (m-1) all
          after = substring (m+2) (length all-1) all
          operator = all!!(m-1)
          m = firstIndex (\(a,b) -> 
                           ((a=='&') || (a=='|')) && (b==1))  
              $ parOpen all
  all@('!':xs) -> Not (str2WFFHelp $ substring 3 (length all -1) all)
  all@('[':xs) ->
    if (last xs /= ']') 
    then error "Parse error/n"
    else if (operator == '=')
         then Imp (str2WFFHelp before) (str2WFFHelp after)
    else if (operator == '<')
         then Equ (str2WFFHelp before) (str2WFFHelp after)
         else error "Parse error\n"
    where before = substring 2 (m-2) all
          after = substring (m+4) (length all-1) all
          operator = all!!(m-1)
          m = firstIndex (\(a,b) ->
                           ((a=='=') || (a=='<')) && (b==0))
              $ brackOpen all
  all -> WFFvar all

-- ==================================================  
-- helper function to str2WFF:  
-- finds the number of open paranteses (n'(') - (n')')
-- before for all indices
-- we want to split the string at &&'s or ||'s with parOpen-value 1  
--parOpen :: String -> [(Char,Int)]
parOpen xs = fst $ (foldl (\(acc,par) x -> 
                           if (x=='(') 
                           then (acc ++ [(x,par)],par+1)
                           else if (x==')')
                                then (acc ++ [(x,par)],par-1)
                                else (acc ++ [(x,par)],par))
             ([],0) xs)
                                     

brackOpen xs = fst $ (foldl (\(acc,par) x -> 
                           if (x=='[') 
                           then (acc ++ [(x,par)],par+1)
                           else if (x==']')
                                then (acc ++ [(x,par)],par-1)
                                else (acc ++ [(x,par)],par))
             ([],0) xs)


-- ==================================================  
-- another helper function to str2WFF
-- returns first index satisfying pred
firstIndex pred xs = firstIndexHelp pred xs 1 xs
firstIndexHelp pred [] acc bug = error ("No such index  in " ++ (show bug))
firstIndexHelp pred (x:xs) acc bug = if (pred x) then acc
                       else firstIndexHelp pred xs (acc+1) bug

-- ==================================================  
-- str2WFF helper
--substring :: Int -> Int -> String -> String
substring x y st = if (x<1 && y>(length st)) 
                   then 
                     error "**ERROR**Negative or too large index\n"
                   else if (y<x) 
                        then
                          error "**ERROR**Last index > first index \n"
                   else (take (y-x+1) . drop (x-1)) st
-- ================================================== 


simplify :: WFF -> WFF
simplify (Not (Not a)) = a
simplify (Or TRUE _) = TRUE
simplify (Or _ TRUE) = TRUE
simplify (Or FALSE y) = (simplify y)
simplify (Or y FALSE) = (simplify y)
simplify (Or x y) = if (x==y) 
                    then (simplify x)
                    else Or (simplify x) (simplify y)
simplify (And FALSE _) = FALSE
simplify (And _ FALSE ) = FALSE
simplify (And TRUE y) = (simplify y)
simplify (And y TRUE) = (simplify y)
simplify (And a (Not b)) = if a==b then FALSE  else (And (simplify a) (Not (simplify b)))
simplify (And x y) = if (x==y) 
                     then (simplify x)
                     else And (simplify x) (simplify y)

--simplify (And (Not a) b) =   if a==b then FALSE
--                             else (And (Not (simplify a)) (simplify b))
--simplify (Or a (Not a)) = TRUE
--simplify (Or (Not a) a) = TRUE
simplify x = x
-- ==================================================  
data Theorem = Theorem {
  assumptions :: [WFF] 
  ,claim :: WFF
  } 

-- ==================================================
instance Show Theorem where
  show (Theorem a c) = "claims:\n" ++ foldr (\x acc -> (show x) ++ "\n" ++ acc)
                                        [] a ++ "implies:\n" ++ (show c)

-- ==================================================
-- example theorem
equivTheorem :: Theorem
equivTheorem = Theorem [(Not ((And (WFFvar "p1") (WFFvar "p2"))))] 
               (Or (Not (WFFvar "p1")) (Not (WFFvar "p2")))
               
-- ==================================================
-- valid proof steps
data ProofStep = AndI Int Int 
               | AndEL Int
               | AndER Int
               | E Int Int
                 
data ProofStep2 = AndI2 WFF WFF
                | AndEL2 WFF
                | AndER2 WFF
                | E2 WFF WFF

-- ==================================================
data Proof = Proof {
  proof :: [ProofStep]
  ,theorem :: Theorem
  }

-- ==================================================
data ProofMap = Proof2 {
  proof2 :: [ProofStep2]
  , theorem2 :: Theorem
  }
-- ==================================================      
assumGen :: [WFF] -> [String]
assumGen = map show

applyProofStep2 :: [String]
                   -> ProofStep2
                   -> [String]
applyProofStep2 xs (AndI2 p q) = if not 
                                    ((elem (show p) xs) 
                                     && (elem (show q) xs))
                                    then error
                                         "Nope.\n"
                                 else (show (And p q)):xs

-- ==================================================
applyProofStep :: [WFF] -> ProofStep -> WFF
applyProofStep xs (AndI a b) = And (xs!!a) (xs!!b)
applyProofStep xs (AndEL a) = x where 
  And x y = xs!!a
applyProofStep xs (AndER a) = y where
  And x y = xs!!a
applyProofStep xs (E a b) = if r == p 
                            then q 
                            else error $ "they are not equal!!" ++ "\n"
                                 ++ "WFF at index " ++ (show a)
                                 ++ "!= WFF at index " ++ (show b)
  where And p q = xs!!b
        r = xs!!a

-- ==================================================
check_proof :: Proof  -> Bool
check_proof pr = last (foldl -- [WFF] -> ProofStep -> [WFF]
                       (\props step -> props 
                                       ++ [(applyProofStep props step)]) 
                       (assumptions t)
                       st
                      ) == (claim t)
                   where st = proof pr
                         t = theorem pr
  
-- ==================================================
debugList pr = foldl 
               (\props step -> props 
                               ++ [(applyProofStep props step)]) 
               (assumptions t) 
               st
                 where 
                   st = proof pr
                   t = theorem pr
                         
-- ==================================================
easyTheorem = Theorem [WFFvar "p1", WFFvar "p2"] 
              (And (WFFvar "p1") (WFFvar "p2"))

-- ==================================================
proofOfEasyTheorem = Proof [AndI 0 1] easyTheorem

-- hurray!! the proof evaluates to true!!

-- ==================================================
easyTheorem2 = Theorem [WFFvar "p1", WFFvar "p2", WFFvar "p3"] 
               (And (And (WFFvar "p1") (WFFvar "p2")) (WFFvar "p3"))

-- ==================================================
--proof2 = Proof [AndI 0 1, AndI 3 2] easyTheorem2

-- ==================================================
easyTheorem3 = Theorem [WFFvar "p", And (WFFvar "q") (WFFvar "r")] 
               (And (WFFvar "p") (WFFvar "q"))

-- ==================================================
proof3 = Proof [AndEL 1, AndI 0 2] easyTheorem3

-- ==================================================
-- p && q -> q && p
commutative = Theorem [And (WFFvar "p") (WFFvar "q")] 
              (And (WFFvar "q") (WFFvar "p"))
              
-- ==================================================
commProof = Proof [AndEL 0, AndER 0, AndI 2 1] commutative

--impChain 
-- ==================================================                    
-- example
equivRule :: WFF
equivRule = Equ (Not ((And (WFFvar "p1") (WFFvar "p2"))))
            (Or (Not (WFFvar "p1")) (Not (WFFvar "p2")))

